int GetNumber(DviWidget);
